\newcommand{\sts}{spatial transition system}
%\newcommand{\to}{\rightarrow}
\newcommand{\sumop}{\oplus}
\newcommand{\Bpred}{O}
\newcommand{\At}{At}
\newcommand{\bpred}{p}
\newcommand{\sbs}{spatial behavioral simulation}
\newcommand{\state}{s}
\newcommand{\tstate}{t}
\newcommand{\mypr}{\sqsubseteq}
\newcommand{\swsts}{well-structured spatial transition system}
\newcommand{\wqo}{wqo}
\newcommand{\mieq}{\leq}
\newcommand{\qo}{quasi order}
\newcommand{\Min}{Min}
%Standard definitions and notation for well-quasi-orders (wqo), transition systems, and well-structured transition systems can be found in Appendix \ref{app:wsts}. 
Recall that a \emph{quasi-order} (or, equivalently, preorder) is a reflexive
and transitive relation.

\begin{definition}[Well-quasi-order]
A \emph{well-quasi-order} (wqo) is a quasi-order $\leq$ over a
set $X$ such that, for any infinite sequence $x_0 , x_1 , x_2 \ldots \in X$, there exist indexes $i < j$
such that $x_i \leq x_j$.
\end{definition}

 Note that if $\leq$ is a wqo then any infinite sequence $x_0 , x_1 , x_2 , \ldots$ contains an infinite
increasing subsequence $x_{i_0} , x_{i_1} , x_{i_2} , \ldots$ (with $i_0 < i_1 < i_2 < \ldots$). 
Thus well-quasi-orders exclude the possibility of having infinite strictly decreasing sequences.


We also need a definition for (finitely branching) transition systems. Here and in the following %$\rightarrow^{+}$ (resp. 
$\rightarrow^*$ denotes the 
%transitive (resp. the 
reflexive and transitive
%) 
closure of the relation $\rightarrow$.


\begin{definition}[Transition system]
\label{def:WSTS}
A \emph{transition system} is a structure $TS = (S, \rightarrow)$, where $S$ is a set of states
and $\rightarrow \subseteq  S \times S$ is a set of transitions. 
We define $Succ(s)$ as the set $\{s' \in S \mid s \rightarrow s' \}$
of immediate \emph{successors} of $s$. %We say that 
$TS$ is \emph{finitely branching} if, for each $s \in S$,
$Succ(s)$ is finite.
We also define $Pred(s)$ as the set $\{s' \in S \mid s' \rightarrow s\}$ of \emph{immediate predecessors} of $s$,
while $Pred^*(s)$ and $Pred^+(s)$ denote the sets $\{s \in S \mid s' \rightarrow^* s\}$ and  $\{s \in S \mid s' \rightarrow^+ s\}$, respectively, of \emph{predecessors} of $s$.
\end{definition}

\begin{mynotation}
In the rest of the paper, 
and with a slight abuse of notation,
we will  assume the expected point-wise extensions of definitions to sets. 
For instance, 
%we will  use 
%The function 
function $Succ$ just defined on states is extended to sets of states as:
 %, $Pred$, $Pred^*$ and  $Pred^+$
%will also be used  
%on sets, %by assuming 
%that in this case they are defined by 
%the point-wise extension of the above definitions, 
$Succ(S) = \bigcup_{s \in S} Succ(s)$.  
\end{mynotation}










%
% We, now, introduce some notation from \cite{Acciai10}. Let $\At$ be a finite set of \emph{atomic predicates} ranged over $\bpred,\bpred',\ldots$. We let $\mathcal{P}(\At)$ denote the powerset of $\At$. Recall that a \emph{monoid} $(M,\oplus,0_M)$ is a semigroup with $0_M$ as an identity element.
% We then define \emph{spatial transition systems} as follows:
% 
% \begin{definition}[Spatial transition system]\label{def:sts}
% A \emph{spatial transition system} 
% %(\sts) 
% is a tuple
% $STS = (S,{\to,}\sumop, \Bpred)$ where
% % $\mathcal S=(S,{\to,}\sumop, \Bpred)$ where:
% %\begin{enumerate}
% (i)  $(S,\to)$ is a transition system,
% (ii)   $(S,\sumop,0_S)$ is a monoid  for some $0_S\in S$, and
% (iii) $\Bpred:S\to \mathcal P(\At)$ is an \emph{observation function}.
% %\end{enumerate}
% \end{definition}
% 
% The relationship among the transition system, the
% monoid  and the observation function is given by
% the following \emph{spatial-behavioral simulation}.
% %,
% %which is a  weak (bi)simulation for {\sts} with extra conditions concerning $\sumop$ and $\Bpred$.
% 
% \begin{definition}%[Spatial-behavioral simulation]
% \label{def:sbs}
% A \emph{spatial-behavioral simulation} %({\sbs})
%  over a \sts\ $STS=(S,\to,\sumop,\Bpred)$  is a binary relation $\mathcal R\subseteq S\times S$  such that whenever  $\state \:\mathcal R\:\tstate$ then:
% %\begin{enumerate}
% %\item \label{sbs:uno} 
% (i) whenever  $\state\to\state'$ then there exists $\tstate'\in S$ such that $\tstate\to^{*}\tstate'$ and $\state'\: \mathcal R\:\tstate'$;
% %\item \label{sbs:due} 
% (ii) whenever  $\state=\state_1\sumop\state_2$  then there are $\tstate_1,\tstate_2\in S$ such that $\tstate=\tstate_1\sumop\tstate_2$ and $\state_i\:\mathcal R\:\tstate_i$, for $i=1,2$;
% %\item \label{sbs:tre}  
% (iii) $\Bpred(\state)\subseteq\Bpred(\tstate)$. %\vspace*{-0.2cm}
% %\end{enumerate}
% The largest   {\sbs}, denoted  $\mypr$, is a preorder over $S$, called  \emph{spatial-behavioral preorder}.
% \end{definition}





The key tool to 
the decidability of 
%decide 
several properties of computations 
is the notion of \emph{well-structured transition system} \cite{FinkelS01,AbdullaCJT00}. 
This is a transition system equipped with a well-quasi-order on states
which is (upward) compatible with the transition relation. Here we will use a strong version 
of compatibility; hence the following definition.


\begin{definition}[Well-structured transition system] %with strong compatibility]
A \emph{well-struc\-tured transition system with strong compatibility} is a transition system 
$TS = (S, \rightarrow)$, equipped with a quasi-order $\leq$ on $S$, such that the two following conditions hold:
%\vspace{-2mm}
\begin{enumerate}
\item 
 $\leq$ is a well-quasi-order;
\item 
 $\leq$ is strongly (upward) compatible with $\rightarrow$, that is, for all $s_1 \leq t_1$ and all transitions
   $s_1 \rightarrow s_2$ , there exists a state $t_2$ such that $t_1 \rightarrow t_2$ and $s_2 \leq t_2$ holds.
\end{enumerate}
\end{definition}

% The following theorem is a special case of Theorem 4.6 in \cite{FinkelS01} and will be used to obtain our decidability result.
% 
% \begin{theorem}\label{th:Finkel}
% Let $TS = (S, \rightarrow, \leq)$ be a finitely branching, well-structured transition
% system with strong compatibility, decidable $\leq$,  and computable $Succ$. Then the existence
% of an infinite computation starting from a state $s \in S$ is decidable.
% \end{theorem}

Given a quasi-order $\leq$ over $X$, an {\em upward-closed set} is a subset $I\subseteq X$ such that
the following holds: $\forall x,y\in X: (x\in I\wedge x\leq y)\Rightarrow y\in I$. Given $x\in X$, we define its upward closure as $\uparrow x = \{y\in X\mid x\leq y\}$. This notion can be extended to sets as expected: given a set $Y\subseteq X$ we define its upward closure as $\uparrow Y = \bigcup_{y\in Y}\uparrow y$. 

\begin{definition}[Finite basis]\label{d:finbas}
A {\em finite basis} of an upward-closed set $I$ is a finite set $B$ such that $I = \bigcup_{x\in B}\uparrow x$.
\end{definition}

%In our case t
The notion of basis is particularly important when considering 
the basis of the predecessor of a state in a transition system. More precisely, we are interested in  \emph{effective} pred-basis as defined below.

\begin{definition}[Effective pred-basis]\label{d:efpb}
A well-structured transition system has {\em effective pred-basis} if there exists an algorithm such that, for any state $s\in S$, it returns the set $pb(s)$ which is a finite basis of $\uparrow Pred(\uparrow s)$.
\end{definition}

The following proposition is a special case of Proposition 3.5 
in \cite{FinkelS01}.
\begin{proposition} \label{predcomp}
Let $TS = (S,\rightarrow,\leq)$ be a finitely branching,
well-structured transition system
with strong compatibility, decidable $\leq$ and effective pred-basis.
It is possible to compute a finite basis of $Pred^*(I)$ for any upward-closed set $I$
given via a finite basis.
\end{proposition}

% We will also need a result due to Higman \cite{Higman52} which allows to extend a well-quasi-order
% from a set $S$ to the set of the finite sequences on $S$. More precisely, given a set $S$ let
% us denote by $S^*$ the set of finite sequences built by using elements in $S$. 
% We can define a quasi-order on $S^*$ as follows.
% 
% \begin{definition}\label{def:eqwqo}
% Let $S$ be a set and $\leq$ a quasi-order over $S$. The relation $\leq_*$ over $S^*$
% is defined as follows. Let $t, u \in S^*$, with $t = t_1 t_2 \ldots t_m$ and $u = u_1 u_2 \ldots u_n$. 
% We have that $t \leq_* u$ if and only if there exists an injection $f$ from $\{1, 2, \ldots m \}$ 
% to $\{1, 2, \ldots n\}$ such that $t_i \leq u_{f (i)}$ and $f(i) < f(i+1)$ 
% for $i = 1, \ldots , m-1$.
% \end{definition}
% 
% The relation $\leq_*$ is clearly a quasi-order over $S^*$. 
% It is also a wqo, since we have the following result.
% 
% \begin{lemma}[Higman] %\cite{Higman52}] 
% \label{lem:Higman}
% Let $S$ be a set and $\leq$ a wqo over $S$. 
% Then %the relation 
% $\leq_*$ is a wqo over $S^*$.
% \end{lemma}

Finally we will use the following proposition, whose proof is immediate.

\begin{proposition}\label{prop:eqwqo}
Let $S$ be a finite set. Then the equality is a wqo over $S$.
\end{proposition}


%Another 
%An extension to the theory of wqo is needed in the rest of the paper. 
We shall also appeal to the following result.
In \cite{kruskal60}, Kruskal proved that a wqo on a set $S$ can be extended to the set of finite trees whose nodes have labels ranging in $S$; we refer to this as the set of trees \emph{over} $S$.
We first define how to extend a quasi order on a set $S$ to the trees over $S$.
If $t$ is a tree and $n$ a node in $t$, we denote with $label(n)$ the label of the node $n$.

\begin{definition}\label{def:prectr}
  Let $S$ and $\leq$ be a set and a wqo over $S$, respectively. 
  The relation $\leq^{\mathsf{tr}}$ on the set of
trees over $S$ is defined as follows. Let $t, u$ be trees over $S$. We have that $t \leq^{\mathsf{tr}} u$ iff there
exists an injection $f$ from the nodes of $t$ to the ones of $u$ such that:
\begin{enumerate}
 \item Let $m,n$ be nodes in $t$. If $m$ is an ancestor of $n$ then $f(m)$ is an ancestor of $f(n)$.
 \item Let $m,n,p$ be nodes in $t$. If $p$ is the minimal common ancestor of $m$ and $n$ then $f(p)$ is the minimal common ancestor of $f(m)$ and $f(n)$.
 \item Let $n$ be a node in $t$. Then $label(n) \leq label(f(n))$.
\end{enumerate}
\end{definition}

%Similarly as before t
The relation $\leq^{tr}$ is  a quasi-order over the trees over $S$. 
It is also a wqo, since we have the following result.

\begin{theorem}[Kruskal \cite{kruskal60}]\label{lem:kruskal}
   Let $S$ be a set and $\leq$ a wqo over $S$. Then, the relation $\leq^{tr}$ 
is a wqo on the set of trees over $S$.
\end{theorem}



% 
% The definition of a well-structured transition system can be extended to a \sts.  For any
%  \qo\ $\mieq$ over $S$ and  $T\subseteq S$, we say $s\in T$ is a \emph{minimal}
%   element of $T$ if for each $t\in T$, $s\mieq t$; we let $\Min(T)$ denote the set of minimal elements of $T$.
% 
% 
% \begin{definition}[Well-structured spatial transition system]\label{def:swsts}
% A \emph{well-structured spatial transition system} %(\swsts)
% is a \sts\ $STS=(S,\to,\sumop,\Bpred)$ equipped with a
%  \wqo\ $\mieq$ over $S$ satisfying the following conditions:
% %\begin{enumerate}
% (i) $\mieq$ is a \sbs,
% %Deriva dal fatto che esiste l'elemento neutro del monoide
% %\item $\state\sumop\tstate\maeq \state$ and $\state\sumop\tstate\maeq\tstate$, for any $\state,\tstate\in S$;
% (ii) whenever $\state\mieq \state'$ then for each $t$
%  $\state\sumop\tstate\mieq\state'\sumop\tstate$ and
%   $\tstate\sumop\state\mieq\tstate\sumop\state'$, and
% % \item the partial order induced by $\mieq$ is a sup-semilattice. NON VALE PER IL CCS
% (iii) $0_S\in \Min(S)$.
% %\end{enumerate}
% \end{definition}















